update{-}spec{-}decl(${\it upd}$; ${\it ds}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$z$:Id. ($z$ $\in$ update{-}spec{-}vars(${\it upd}$)) $\Rightarrow$ ($\uparrow$fpf{-}dom(id{-}deq; $z$; ${\it ds}$))